structure Prfgen1 =
struct
  structure P = Proof1
  structure Asm = Assem
  structure A = Assert
  structure S2A = Svc2avc1
  structure T = Temp
  structure Tr = Transp
  structure LCoq = LCoqize1

  fun mapToAddr (id) = 0 (* cheat compiler! *)
  fun reg2exp(reg) = 
      let fun handlereg(Asm.Eax) = A.Eax
	    | handlereg(Asm.Ebx) = A.Ebx
	    | handlereg(Asm.Ecx) = A.Ecx
	    | handlereg(Asm.Edx) = A.Edx
	    | handlereg(Asm.Esi) = A.Esi
	    | handlereg(Asm.Edi) = A.Edi
	    | handlereg(Asm.Esp) = A.Esp
	    | handlereg(Asm.Ebp) = A.Ebp
      in handlereg(reg)
      end

(* update State: state*instr-> state *)
  fun upState instr st= 
      let fun rf(state:A.state) = #1 state
	  fun hp(state:A.state) = #2 state
	  fun mchinstr(Asm.Addr(r1,r2)) = 
	      let val updexp2 = A.Plus(A.Sel(rf(st),reg2exp(r2)),
				       A.Sel(rf(st),reg2exp(r1)))
		  val st' = (A.Upd(rf(st),reg2exp(r2),updexp2),hp(st))
	      in st'
	      end
	    | mchinstr(Asm.Addz(imm,r2)) = 
	      let val updexp2 = A.Plus(A.Sel(rf(st),reg2exp(r2)),
				       A.IntNum(imm))
		  val st' = (A.Upd(rf(st),reg2exp(r2),updexp2),hp(st))
	      in st'
	      end
	    | mchinstr(Asm.Subr(r1,r2)) = 
	      let val updexp2 = A.Minus(A.Sel(rf(st),reg2exp(r2)),
				       A.Sel(rf(st),reg2exp(r1)))
		  val st' = (A.Upd(rf(st),reg2exp(r2),updexp2),hp(st))
	      in st'
	      end
	    | mchinstr(Asm.Subz(imm,r2)) = 
	      let val updexp2 = A.Minus(A.Sel(rf(st),reg2exp(r2)),
				       A.IntNum(imm))
		  val st' = (A.Upd(rf(st),reg2exp(r2),updexp2),hp(st))
	      in st'
	      end
	    | mchinstr(Asm.Mulr(r1,r2)) = 
	      let val updexp2 = A.Times(A.Sel(rf(st),reg2exp(r2)),
				       A.Sel(rf(st),reg2exp(r1)))
		  val st' = (A.Upd(rf(st),reg2exp(r2),updexp2),hp(st))
	      in st'
	      end
	    | mchinstr(Asm.Mulz(imm,r2)) = 
	      let val updexp2 = A.Times(A.Sel(rf(st),reg2exp(r2)),
				       A.IntNum(imm))
		  val st' = (A.Upd(rf(st),reg2exp(r2),updexp2),hp(st))
	      in st'
	      end
	    | mchinstr(Asm.Push(r1)) = 
	      let val rfupdexp2 = A.Minus(A.Sel(rf(st),A.Esp),A.IntNum(4))
		  val rf' = A.Upd(rf(st),A.Esp,rfupdexp2)
		  val hp' = A.Upd(hp(st),A.Sel(rf(st),A.Esp),
				  A.Sel(rf(st),reg2exp(r1)))
		  val st' = (rf',hp')
	      in st'
	      end
	    | mchinstr(Asm.Pop(r1)) = 
	      let val updesp = A.Upd(rf(st), A.Esp,
				     A.Plus(A.Sel(rf(st),A.Esp),A.IntNum(4)))
		  val rf' = A.Upd(updesp,reg2exp(r1),
				  A.Sel(hp(st),A.Sel(rf(st),A.Esp)))
		  val st' = (rf',hp(st))
	      in st'
	      end
	    | mchinstr(Asm.Xchg(r1,r2)) = 
	      let val rf1 = A.Upd(rf(st),reg2exp(r1),A.Sel(rf(st),reg2exp(r2)))
		  val st' = (A.Upd(rf1,reg2exp(r2),A.Sel(rf(st),reg2exp(r1))),hp(st))
	      in st'
	      end
	    | mchinstr(Asm.Leal(str,r1)) = 
	      let val st' = (A.Upd(rf(st),reg2exp(r1),A.Addr(mapToAddr(str))),hp(st))
	      in st'
	      end
	    | mchinstr(Asm.Leab(ofaddr,r1,r2)) = (*WIP*)
	      let val addr = A.Plus(A.Sel(rf(st),reg2exp(r1)),
				    A.IntNum(ofaddr))
		  val st' = (A.Upd(rf(st),reg2exp(r2),addr),hp(st))
	      in st'
	      end
	    | mchinstr(Asm.Movr(r1,r2)) = 
	      let val st' = (A.Upd(rf(st),reg2exp(r2),A.Sel(rf(st),reg2exp(r1)))
			     ,hp(st))
	      in st'
	      end
	    | mchinstr(Asm.Movz(imm,r2)) = 
	      let val st' = (A.Upd(rf(st),reg2exp(r2),A.IntNum(imm)),hp(st))
	      in st'
	      end
	    | mchinstr(Asm.Movld(imm,r1,r2)) = 
	      let val updexp1 = A.Sel(hp(st),A.Plus(A.Sel(rf(st),reg2exp(r1)),
						    A.IntNum(imm)))
		  val st' = (A.Upd(rf(st),reg2exp(r2),updexp1),hp(st))
	      in st'
	      end
	    | mchinstr(Asm.Movst(r1,imm,r2)) = 
	      let val updexp1 = A.Plus(A.Sel(rf(st),reg2exp(r2)),A.IntNum(imm))
		  val hp' = A.Upd(hp(st),updexp1,A.Sel(rf(st),reg2exp(r1)))
		  val st' = (rf(st),hp')
	      in st'
	      end
            | mchinstr(Asm.Ret) =
              let val rf' = A.Upd(rf(st), A.Esp,
				 A.Plus(A.Sel(rf(st),A.Esp),A.IntNum(4)))
                  val st' = (rf', hp(st))
              in  st'
              end
	    | mchinstr(_) = st
      in mchinstr(instr)
      end


  fun prf_gen pre (cd_b, ass ,prf_b) post cb specs vcname = 
      let fun gen ((Asm.Jmp(l))::cb') =
              let val postopt = A.getspec l specs
                  val post = case (!postopt)
                              (* WIP : should raise fail *)
                              of  NONE => (raise Fail ("Impossible! No such label: "^l^"\n"); (fn st:A.state => A.True))
                                | SOME(a) => a
                  val st = upState (Asm.Jmp(l))
                  val a = (fn st_init:A.state => post (st st_init)) 
              in  case cb'
                   of  [] => ([Asm.Jmp(l)], pre, P.WF_jmp (l,(pre, post, vcname)))
                     | _ => let val new_prf_b = P.WF_jmp (l,(a, post, ""))
                                val new_cd_b = [Asm.Jmp(l)]
                            in  prf_gen pre (new_cd_b, a, new_prf_b) a cb' specs vcname
                            end 
              end
            | gen (Asm.Ret :: cb') = (* Work In Progress *)
              let (*get post condition*)
                  val postopt = A.getspec "post_condition" specs
                  val post = case !postopt
                              of  NONE => (raise Fail ("Impossible! No such label: post_condition \n"); (fn st:A.state => A.True))
                                (* (print ("Impossible! No such label: "^l^"\n"); (fn st:A.state => A.True)) *)
                                | SOME(a) => a
                  (* generate a *)
                  val st = upState (Asm.Ret)
                  val a = (fn st_init:A.state => post (st st_init)) 
              in  case cb'
                   of  [] => ([Asm.Ret], pre, P.WF_trivial)  (*WIP*)
                     | _  => let val new_prf_b = P.WF_trivial (*WIP*)
                                 val new_cd_b = [Asm.Ret]
                             in  prf_gen pre (new_cd_b, a, new_prf_b) a cb' specs vcname
                             end
              end
            | gen ((Asm.Addr(r1, r2))::cb') =
              let val st = upState (Asm.Addr(r1,r2))
                  val a = (fn st_init:A.state => post (st st_init))
              in  case cb'
                   of  [] => ((Asm.Addr(r1,r2))::cd_b, pre ,(P.WF_addr (r1, r2, (cd_b, prf_b), (pre, post, vcname))))
                     | _ => let val new_prf_b = P.WF_addr (r1, r2, (cd_b, prf_b), (a, post, "")) 
                                val new_cd_b = (Asm.Addr(r1,r2))::cd_b
                            in  prf_gen pre (new_cd_b, a, new_prf_b) a cb' specs vcname
                            end
              end
            | gen ((Asm.Movr(r1, r2))::cb') =
              let val st = upState (Asm.Movr(r1,r2))
                  val a = (fn st_init:A.state => post (st st_init))
              in  case cb'
                   of  [] => ((Asm.Movr(r1,r2))::cd_b, pre ,(P.WF_movr (r1, r2, (cd_b, prf_b), (pre, post, vcname))))
                     | _ => let val new_prf_b = P.WF_movr (r1, r2, (cd_b, prf_b), (a, post, "")) 
                                val new_cd_b = (Asm.Movr(r1,r2))::cd_b
                            in  prf_gen pre (new_cd_b, a, new_prf_b) a cb' specs vcname
                            end
              end
            | gen ((Asm.Subz(i, r))::cb') =
              let val st = upState (Asm.Subz(i,r))
                  val a = (fn st_init:A.state => post (st st_init))
              in  case cb'
                   of  [] => ((Asm.Subz(i,r))::cd_b, pre ,(P.WF_subz (i, r, (cd_b, prf_b), (pre, post, vcname))))
                     | _ => let val new_prf_b = P.WF_subz (i, r, (cd_b, prf_b), (a, post, "")) 
                                val new_cd_b = (Asm.Subz(i,r))::cd_b
                            in  prf_gen pre (new_cd_b, a, new_prf_b) a cb' specs vcname
                            end
              end
            | gen ((Asm.Push r)::cb') =
              let val st = upState (Asm.Push r)
                  val a = (fn st_init:A.state => post (st st_init))
              in  case cb'
                   of  [] => ((Asm.Push r)::cd_b, pre ,(P.WF_push (r, (cd_b, prf_b), (pre, post, vcname))))
                     | _ => let val new_prf_b = P.WF_push (r, (cd_b, prf_b), (a, post, "")) 
                                val new_cd_b = (Asm.Push r)::cd_b
                            in  prf_gen pre (new_cd_b, a, new_prf_b) a cb' specs vcname
                            end
              end
            (* WIP should raise Fail *)
            | gen (i::cb') = (print "work in progress!\n"; (i::cd_b, (fn st_init:A.state => A.True), P.WF_trivial))
            | gen [] = (raise Fail "impossible!"; (cd_b, (fn st_init:A.state =>A.True), P.WF_trivial))
      in  gen cb
      end


  (* generate the proof of the current instructions in current code block, 
   * because that the current code block has no pre-condition,
   * this function also generate a precondition for it
   *
   * (cb_b, ass, prf_b): sub-proof of current code block which can be used in generating current instructions proof.
   *                     this cb_b is in positive order.
   * post: post condition of the current instruction
   * cb: current instructions, in negative order.
   * specs: real specifications
   * lab: label of current code block, it is used to insert generated pre-condition of the current code block
   *)
  fun prf_gen_no_pre (cd_b, ass, prf_b) post cb specs lab = 
      let fun gen ((Asm.Jmp(l))::cb') =
              let (* get current post-condition *)
                  val postopt = A.getspec l specs
                  val post = case !postopt
                              (* WIP: should raise Fail *)
                              of  NONE => (raise Fail ("Impossible! No such label: "^l^"\n"); (fn st:A.state => A.True))
                                (* (print ("Impossible! No such label: "^l^"\n"); (fn st:A.state => A.True)) *)
                                | SOME(a) => a
                  (*generate pre-condition "a" of the current instruction *)
                  val st = upState (Asm.Jmp(l))
                  val a = (fn st_init:A.state => post (st st_init)) 
              in  case cb'
                   of  [] => (*if the code block has only a jmp instruction, then a is the precondition of the code block*)
                             let val pre = A.getspec lab specs
                                 val _ = pre := (SOME a) 
                             in  (* return the proof: code block, pre-condition, proof-term*)
                                 ([Asm.Jmp l], a, P.WF_jmp (l,(a, post, "")))
                             end
                     | _ => (* if the code block has other instructions, then packed the current proof as a sub-proof
                             * of the hole code block's proof. and continue to generate other sub-proof.*)
                            let val new_prf_b = P.WF_jmp (l, (a, post, ""))
                                val new_cd_b = [Asm.Jmp l]
                            in  prf_gen_no_pre (new_cd_b, a, new_prf_b) a cb' specs lab
                            end 
              end

            | gen (Asm.Ret :: cb') = (* Work In Progress *)
              let (*get post condition*)
                  val postopt = A.getspec "post_condition" specs
                  val post = case !postopt
                              (* WIP: should raise Fail *)
                              of  NONE => (raise Fail ("Impossible! No such label: post_condition \n"); (fn st:A.state => A.True))
                                (* (print ("Impossible! No such label: "^l^"\n"); (fn st:A.state => A.True)) *)
                                | SOME(a) => a
                  (* generate a *)
                  val st = upState (Asm.Ret)
                  val a = (fn st_init:A.state => post (st st_init)) 
              in  case cb'
                   of  [] => let val pre = A.getspec lab specs
                                 val _ = pre := (SOME a) 
                             in ([Asm.Ret], a, P.WF_trivial)  (*WIP*)
                             end
                     | _  => let val new_prf_b = P.WF_trivial (*WIP*)
                                 val new_cd_b = [Asm.Ret]
                             in  prf_gen_no_pre (new_cd_b, a, new_prf_b) a cb' specs lab
                             end
              end

            | gen ((Asm.Addr(r1, r2))::cb') =
              let val st = upState (Asm.Addr(r1,r2))
                  val a = (fn st_init:A.state => post (st st_init))
              in  case cb'
                   of  [] =>  let val pre = A.getspec lab specs
                                  val _ = pre := (SOME a) 
                             in (((Asm.Addr (r1, r2))::cd_b), a, P.WF_addr (r1, r2, (cd_b, prf_b), (a, post, "")))
                             end
                     | _ => let val new_prf_b = P.WF_addr (r1, r2, (cd_b, prf_b), (a, post, ""))
                                val new_cd_b = (Asm.Addr (r1, r2))::cd_b 
                            in  prf_gen_no_pre (new_cd_b, a, new_prf_b) a cb' specs lab
                            end
              end

            | gen ((Asm.Movr(r1, r2))::cb') =
              let val st = upState (Asm.Movr(r1,r2))
                  val a = (fn st_init:A.state => post (st st_init))
              in  case cb'
                   of  [] =>  let val pre = A.getspec lab specs
                                  val _ = pre := (SOME a) 
                             in (((Asm.Movr (r1, r2))::cd_b), a, P.WF_movr (r1, r2, (cd_b, prf_b), (a, post, "")))
                             end
                     | _ => let val new_prf_b = P.WF_movr (r1, r2, (cd_b, prf_b), (a, post, ""))
                                val new_cd_b = (Asm.Movr (r1, r2))::cd_b 
                            in  prf_gen_no_pre (new_cd_b, a, new_prf_b) a cb' specs lab
                            end
              end

            | gen ((Asm.Subz(i, r))::cb') =
              let val st = upState (Asm.Subz(i,r))
                  val a = (fn st_init:A.state => post (st st_init))
              in  case cb'
                   of  [] =>  let val pre = A.getspec lab specs
                                  val _ = pre := (SOME a) 
                             in (((Asm.Subz (i, r))::cd_b), a, P.WF_subz (i, r, (cd_b, prf_b), (a, post, "")))
                             end
                     | _ => let val new_prf_b = P.WF_subz (i, r, (cd_b, prf_b), (a, post, ""))
                                val new_cd_b = (Asm.Subz (i, r))::cd_b 
                            in  prf_gen_no_pre (new_cd_b, a, new_prf_b) a cb' specs lab
                            end
              end

            | gen ((Asm.Push r)::cb') =
              let val st = upState (Asm.Push r)
                  val a = (fn st_init:A.state => post (st st_init))
              in  case cb'
                   of  [] =>  let val pre = A.getspec lab specs
                                  val _ = pre := (SOME a) 
                             in (((Asm.Push r)::cd_b), a, P.WF_push (r, (cd_b, prf_b), (a, post, "")))
                             end
                     | _ => let val new_prf_b = P.WF_push (r, (cd_b, prf_b), (a, post, ""))
                                val new_cd_b = (Asm.Push r)::cd_b 
                            in  prf_gen_no_pre (new_cd_b, a, new_prf_b) a cb' specs lab
                            end
              end
            | gen (i::cb') = (print "work in progress!\n"; (i::cd_b, (fn st_init:A.state =>A.True), P.WF_trivial)) (*WIP*)
            | gen [] = (raise Fail "impossible!"; (cd_b, (fn st_init:A.state =>A.True), P.WF_trivial))
      in  gen cb
      end

  (* get the code block which is marked by lab in the code list,
   * NOTICE: the generate code block is in negative order.  
   * lab: label, mark the current code block 
   * code: all the assembly code list (positive order)
   *)
  fun get_cb code lab =
      let (* get the start of the code block *)
          fun getlab [] = (raise Fail "no such lab in codes!"; [])
            | getlab ((Asm.Label(l, a))::code') = if (l = lab)
                                                  then code'
                                                  else getlab code'
            | getlab (_::code') = getlab code'
          val begin = getlab code
          val cb = ref []
          (* from the start of the code block to find the end of the code block,
           * generate the current code block that in negative order
           *)
          fun get [] = (raise Fail ("there is no instruction?");())
            | get (Asm.Label(l,_)::code') = (raise Fail ("should not meet a label: "^l); ())
            | get (Asm.Section(_)::code') = (raise Fail ("should not meet a section");())
            | get ((Asm.Jmp l) :: code') = (cb := (Asm.Jmp l) ::(!cb))
            | get (Asm.Call f :: code') = (cb := (Asm.Call f) :: (!cb))
            | get (Asm.Ret :: code') = (cb := (Asm.Ret)::(!cb))
            | get (i::code') = (cb := i::(!cb); (get code'))
      in  get begin;
          !(cb)
      end

  (* generate all the proof of the code block whose labels are in the spec_index, and
   * also generate every code blocks' pre-conditions.
   *
   * spec_index: labels that has no specification, 
   * code: positive order assembly code (all the code)
   * specs: real specification (current all specification)
   *)
  fun prf_list_gen_1 spec_index code specs =
      let val prf_list = ref [] (* proof list *)
          (* generate all the proof of the code blocks whose label is in the the arguments label list *)
          fun gen (l::speci) = 
              let val cb = get_cb code l (* get current code block (negative order)*)
                  (* get the label of the post-condition of the code block *)
                  val l1 = case cb 
                            of (Asm.Jmp(l2)::cb') => l2
                             | (Asm.Ret::cb')=> "post_condition" (*WIP*)
                             | _ => (raise Fail "impossible, last instruction is not a jmp!"; "bogus")
                  fun eql x = if (x = l1)
                              then true
                              else false
              in  (* if the post-condition's label has no real specification, then put the code block in the tail
                   * of the processing list and pick another code block to process 
                   *)
                  if (List.exists eql (l::speci))
                  then gen (speci@[l])
                  else let (*get the post condition of the code block*) 
                           val post = fn s:A.state => A.True (* no use, cheat compiler *) 
(*                         val post' = A.getspec l1 specs 
                           val post = case (!post') 
                                       of  NONE => (raise Fail ("impossible! no such specification: "^l1^"\n"); fn s:A.state => A.True)
                                         | SOME (a) => a
*)
                           (* generate the proof and precondition of the code block *)
                           val proof = prf_gen_no_pre ([], post, P.WF_trivial) post cb specs l
                       in  prf_list := ((l, proof):: !prf_list); (* put proof and its label into the proof list *)
                           gen speci (*continue to generate other code block's proof until the speci is empty *)
                       end
              end
            | gen [] = ()
      in  gen spec_index; (* generate all the code blocks' proof in the spec_index *)
          !prf_list (* return the proof list*)
      end

  fun prf_list_gen_2 spec_index code specs =
      let val prf_list = ref []
          fun gen (l::speci) = 
              let val cb = get_cb code l
                  val l1 = case cb 
                            of (Asm.Jmp(l2)::cb') => l2
                             | (Asm.Ret::cb')=> "post_condition" (*WIP*)
                             | _ => (raise Fail "impossible, last instruction is not a jmp!\n"; "bogus") (*WIP should raise Fail*)
              in  let val post =  fn s:A.state => A.True  (* no use, cheat compiler *) 
(*                    val post' = A.getspec l1 specs
                      val post = case (!post') 
                                  of  NONE => (raise Fail ("impossible! no such specification: "^l1^"\n"); fn s:A.state => A.True)
                                    | SOME (a) => a
*)
                      val pre' = A.getspec l specs
                      val pre = case (!pre')
                                 of  NONE => (raise Fail ("impossible! no such specification: "^l); fn s:A.state => A.True)
                                   | SOME (a) => a
                      val proof = prf_gen pre ([], post, P.WF_trivial) post cb specs l
                  in  prf_list := ((l, proof):: !prf_list);
                      gen speci
                  end
              end
            | gen [] = ()
      in  gen spec_index;
          !prf_list
      end

  fun lookupct_prf_gen (spec_name, spec) l a1 = 
      let fun nullemit str:string = str
	  val ct = List.map (fn (str_spec, lic) => (str_spec^"_asst", lic)) spec
	  val newl = String.map LCoq.filt l (*substite . to _ in label's name*)
	  (* lookup corresponding label number *)
	  val lnum' = case (LCoq.lkup spec newl)
		       of SOME(l') => l'
			| NONE => (raise Fail "There is no such label!"; 0)
	  val a1' = newl^"_asst"
	  fun hd_eq ict il ia = 
	      let val ict' = LCoq.pr_chty nullemit ict
		  val s_il = Int.toString(il)
	      in P.App(P.App(P.App(P.Var("lookupCT_eq"),P.Var(ict')),P.Var(s_il)),P.Var(ia))
	      end
	  fun hd_neq ict il il' ia ia' pchild = 
	      let val ict' = LCoq.pr_chty nullemit ict
		  val s_il = Int.toString(il)
		  val s_il' = Int.toString(il')
		  val pchild' = P.Ne(P.IntNum(il),P.IntNum(il'))
	      in P.App(P.App(P.App(P.App(P.App(P.App(P.App(P.Var("lookupCT_neq"),P.Var(ict')),
						     P.Var(s_il)),
					       P.Var(s_il')),
					 P.Var(ia)),
				   P.Var(ia')),
			     pchild),
		       pchild')
	      end
	  fun wk_ct lic' s_a ((s_spec, lic):: ls) = if lic = lic' 
						    then hd_eq ls lic' s_a
						    else (let val p_child = wk_ct lic' s_a ls 
							  in hd_neq ls lic lic' s_spec s_a p_child
							  end
							      )
	    | wk_ct lic' s_a [] = P.True
      in wk_ct lnum' a1' ct
      end

  (* translated proof into simple typed lambda calculus style. 
   *
   * prf: the proof to be translated.
   * (spec_name, spec): the specification list's name and the specification index list
   * env: variable environment
   * senv: structure type environment
   *)
  fun prf_blk_gen prf (spec_name, spec) env senv =
      let fun ppp (P.WF_addr(r1, r2, (cb1, prf1), (a, a1, lemma))) =
              let val sub_prf1 = prf_blk_gen prf1 (spec_name, spec) env senv (* Psi |- {a} I *)
                  val sub_prf2 = (* if has no vc, then generate it and its proof, else using vc to generate proof *)
                                 if lemma = ""
                                 then let val tmp_var = T.new_var()
                                          val state = (A.Rf, A.Hp)
                                          val a' = a state
                                          val a'' = S2A.transpp a' (*translate assertion into coq style*)
                                      in  (* forall s, a s -> s1 s *)
                                          P.Abs(("R", P.Rf),P.Abs(("H", P.Hp),P.Abs((tmp_var, P.Prop(a'')),P.Var(tmp_var))))
                                      end
                                 else P.Var(lemma)
                                     (*let fun findvc ((fid, s)::r) = if fid = lemma
				                                      then s
				                                      else findvc r
	                                     | findvc [] = V.True
                                           val svc = findvc svclist
                                           val avcp = S2A.get_vc_proof svc (lemma^"_vc") env senv false 
                                       in  P.Abs(("R",P.Rf),P.Abs(("H", P.Hp),avcp))
                                       end*)
                  val ct = P.Var(spec_name) (*  Psi *)
                  val a' = P.Asst(a)  (* a *)
                  val a1' = P.Asst(a1) (* a1 *)
                  val rs = S2A.transe (Tr.reg2exp r1)  (* rs *)
                  val rd = S2A.transe (Tr.reg2exp r2)  (* rd *)
                  val cb1' = P.Iseq(cb1)  (* sub code block *)
              in  P.App(P.App(P.App(P.App(P.App(P.App(P.App(P.App(P.Var("I_add"), ct), a'), a1'),rd),rs), cb1'), sub_prf2), sub_prf1)
              end
            | ppp (P.WF_jmp (l, (a, a1, lemma))) =
              let val newl = String.map LCoq.filt l (*substite . to _ in label's name*)
                  (* lookup corresponding label number *)
                  val lnum' = case (LCoq.lkup spec newl)
                                 of SOME(l') => l'
                                  | NONE => (raise Fail "There is no such label!"; 0)
                  val lnum = P.Lab(lnum') (*label*)
                  val ct = P.Var(spec_name) (* Psi *)
                  val a' = P.Asst(a)  (* a *)
                  val a1' = P.Asst(a1)  (* a1 *)
                  val subprf1 = lookupct_prf_gen (spec_name, spec) l a1 (* Psi(l) = a1 *)
                  val subprf2 = (* if has no vc, then generate it and its proof, else using vc to generate proof *)
                                if lemma = ""
                                then let val tmp_var = T.new_var()
                                         val state = (A.Rf, A.Hp)
                                         val a' = a state
                                         val a'' = S2A.transpp a'
                                     in  P.Abs(("R", P.Rf),P.Abs(("H", P.Hp),P.Abs((tmp_var, P.Prop(a'')),P.Var(tmp_var))))
                                     end
                                else P.Var(lemma)
              in P.App(P.App(P.App(P.App(P.App(P.App(P.Var("I_jmp") ,ct), a'), a1'), lnum), subprf1), subprf2)
              end

            | ppp (P.WF_subz(i, r, (cb1, prf1), (a, a1, lemma))) =
              let val sub_prf1 = prf_blk_gen prf1 (spec_name, spec) env senv (* Psi |- {a} I *)
                  val sub_prf2 = (* if has no vc, then generate it and its proof, else using vc to generate proof *)
                                 if lemma = ""
                                 then let val tmp_var = T.new_var()
                                          val state = (A.Rf, A.Hp)
                                          val a' = a state
                                          val a'' = S2A.transpp a' (*translate assertion into coq style*)
                                      in  (* forall s, a s -> s1 s *)
                                          P.Abs(("R", P.Rf),P.Abs(("H", P.Hp),P.Abs((tmp_var, P.Prop(a'')),P.Var(tmp_var))))
                                      end
                                 else P.Var(lemma)
                                     (*let fun findvc ((fid, s)::r) = if fid = lemma
				                                      then s
				                                      else findvc r
	                                     | findvc [] = V.True
                                           val svc = findvc svclist
                                           val avcp = S2A.get_vc_proof svc (lemma^"_vc") env senv false 
                                       in  P.Abs(("R",P.Rf),P.Abs(("H", P.Hp),avcp))
                                       end*)
                  val ct = P.Var(spec_name) (*  Psi *)
                  val a' = P.Asst(a)  (* a *)
                  val a1' = P.Asst(a1) (* a1 *)
                  val i' = P.IntNum(i)  (* i *)
                  val rd = S2A.transe (Tr.reg2exp r)  (* rd *)
                  val cb1' = P.Iseq(cb1)  (* sub code block *)
              in  P.App(P.App(P.App(P.App(P.App(P.App(P.App(P.App(P.Var("I_subi"), ct), a'), a1'),rd),i'), cb1'), sub_prf2), sub_prf1)
              end

            | ppp (P.WF_push(r, (cb1, prf1), (a, a1, lemma))) =
              let val sub_prf1 = prf_blk_gen prf1 (spec_name, spec) env senv (* Psi |- {a} I *)
                  val sub_prf2 = (* if has no vc, then generate it and its proof, else using vc to generate proof *)
                                 if lemma = ""
                                 then let val tmp_var = T.new_var()
                                          val state = (A.Rf, A.Hp)
                                          val a' = a state
                                          val a'' = S2A.transpp a' (*translate assertion into coq style*)
                                      in  (* forall s, a s -> s1 s *)
                                          P.Abs(("R", P.Rf),P.Abs(("H", P.Hp),P.Abs((tmp_var, P.Prop(a'')),P.Var(tmp_var))))
                                      end
                                 else P.Var(lemma)
                                     (*let fun findvc ((fid, s)::r) = if fid = lemma
				                                      then s
				                                      else findvc r
	                                     | findvc [] = V.True
                                           val svc = findvc svclist
                                           val avcp = S2A.get_vc_proof svc (lemma^"_vc") env senv false 
                                       in  P.Abs(("R",P.Rf),P.Abs(("H", P.Hp),avcp))
                                       end*)
                  val ct = P.Var(spec_name) (*  Psi *)
                  val a' = P.Asst(a)  (* a *)
                  val a1' = P.Asst(a1) (* a1 *)
                  val rs = S2A.transe (Tr.reg2exp r)  (* rd *)
                  val cb1' = P.Iseq(cb1)  (* sub code block *)
              in  P.App(P.App(P.App(P.App(P.App(P.App(P.App(P.Var("I_subi"), ct), a'), a1'),rs), cb1'), sub_prf2), sub_prf1)
              end

            | ppp (P.WF_movr(r1, r2, (cb1, prf1), (a, a1, lemma))) =
              let val sub_prf1 = prf_blk_gen prf1 (spec_name, spec) env senv (* Psi |- {a} I *)
                  val sub_prf2 = (* if has no vc, then generate it and its proof, else using vc to generate proof *)
                                 if lemma = ""
                                 then let val tmp_var = T.new_var()
                                          val state = (A.Rf, A.Hp)
                                          val a' = a state
                                          val a'' = S2A.transpp a' (*translate assertion into coq style*)
                                      in  (* forall s, a s -> s1 s *)
                                          P.Abs(("R", P.Rf),P.Abs(("H", P.Hp),P.Abs((tmp_var, P.Prop(a'')),P.Var(tmp_var))))
                                      end
                                 else P.Var(lemma)
                                     (*let fun findvc ((fid, s)::r) = if fid = lemma
				                                      then s
				                                      else findvc r
	                                     | findvc [] = V.True
                                           val svc = findvc svclist
                                           val avcp = S2A.get_vc_proof svc (lemma^"_vc") env senv false 
                                       in  P.Abs(("R",P.Rf),P.Abs(("H", P.Hp),avcp))
                                       end*)
                  val ct = P.Var(spec_name) (*  Psi *)
                  val a' = P.Asst(a)  (* a *)
                  val a1' = P.Asst(a1) (* a1 *)
                  val rs = S2A.transe (Tr.reg2exp r1)  (* rs *)
                  val rd = S2A.transe (Tr.reg2exp r2)  (* rd *)
                  val cb1' = P.Iseq(cb1)  (* sub code block *)
              in  P.App(P.App(P.App(P.App(P.App(P.App(P.App(P.App(P.Var("I_mov"), ct), a'), a1'),rd),rs), cb1'), sub_prf2), sub_prf1)
              end
            | ppp _ = P.True (*WIP*) 
      in ppp prf
      end

  (* generate well-formedness lemma 
   *
   * cb: current code block, in positive order.
   * spec_name: the specification list's name
   * a: the pre-condition of the current code block
   *)
  fun lemma_gen cb spec_name a=
      let val codeheapty = P.Var(spec_name)  (*code heap type*)
          val infer_name = P.Var("infer") (*inference rule name*)
          val is = P.Iseq(cb)  (*code block*)
          val a' = P.Asst(a)   (* pre-condition*)
      in P.App(P.App(P.App(infer_name,codeheapty),a'), is)  (* Psi |- {a} is  *)
      end


  (* generate lemma and proof of a code block's well-formedness.
   *
   * env: variable enironment
   * senv: structure type environment 
   * spec_name: specification list's name
   * spec: specification index list
   * lab: the code block's lab
   * cb: the code block's code
   * a: the pre-condition of the code block
   * prf: the proof of the well-formedness lemma.
   *)
  fun gen_wf_lemma env senv (spec_name, spec) (lab, (cb, a, prf)) =
      let (* generate well-formedness lemma *)
          val lemma = lemma_gen cb spec_name a
          (* generate proof of the lemma *)
          val proof = prf_blk_gen prf (spec_name, spec) env senv
      in  (lab, lemma, proof)  (*return (lab, lemma, proof)*)
      end

end
